\begin{tabbing}
action{-}rename(${\it rainv}$;${\it rtinv}$;$a$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Case $a$ of\+
\\[0ex]inl($x$) $\Rightarrow$ inl($x$)
\\[0ex]inr($p$) $\Rightarrow$ kindcase\=(1of($p$)\+
\\[0ex]; $a$.\=Case ${\it rainv}$($a$) of\+
\\[0ex]inl($b$) $\Rightarrow$ inr($\langle$locl($b$)$,\,$2of($p$)$\rangle$)
\\[0ex]inr($b$) $\Rightarrow$ inl($\cdot$)
\-\\[0ex]; $l$,${\it tg}$.\=Case ${\it rtinv}$(${\it tg}$) of\+
\\[0ex]inl($t$) $\Rightarrow$ inr($\langle$rcv($l$,$t$)$,\,$2of($p$)$\rangle$)
\\[0ex]inr($b$) $\Rightarrow$ inl($\cdot$) )
\-\-\-
\end{tabbing}